package river_city_ransom.contracts;


import java.util.ArrayList;
import java.util.List;

import exceptions.ComposantError;
import exceptions.InvariantError;
import exceptions.PostconditionError;
import exceptions.PreconditionError;
import river_city_ransom.decorators.GestionCombat_D;
import river_city_ransom.services.Bloc;
import river_city_ransom.services.Dimensions;
import river_city_ransom.services.Equipable;
import river_city_ransom.services.Gangster;
import river_city_ransom.services.GestionCombat;
import river_city_ransom.services.Objet;
import river_city_ransom.services.Personnage;
import river_city_ransom.services.PersonnageJouable;
import river_city_ransom.services.Terrain;
import river_city_ransom.types.BlocType;
import river_city_ransom.types.Commande;
import tools.Toolbox;

public class GestionCombat_C extends GestionCombat_D{

	public GestionCombat_C(GestionCombat delegate) {
		super(delegate);
	}

	/** __________________________________________________________ INVARIANTS */
	public void checkInvariants() throws ComposantError {
		boolean inv;

		/*
		 * equipable1 appartient à {alex(), ryan(), slick(),  gangsters()},
		 * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \ equipable1
	 	collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) 
														<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||
														(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) 
														<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||
														(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) 
														<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||
											  = false sinon
		 */

		Equipable equipable1 = alex();
		Equipable equipable2 = ryan();
		if( (equipable1.dimensions().largeur() + equipable2.dimensions().largeur())/2 <= (equipable1.position().x() - equipable2.position().x())
				|| (equipable1.dimensions().profondeur() + equipable2.dimensions().profondeur())/2 <= (equipable1.position().y() - equipable2.position().y())
				|| (equipable1.dimensions().hauteur() + equipable2.dimensions().hauteur())/2 <= (equipable1.position().z() - equipable2.position().z())
				){
			inv = collision(equipable1, equipable2) == true;
			if(!inv){
				throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
						+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
						+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
						+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
						+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
						+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
						+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
						+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
						+	" = false sinon");
			}
		}else{
			inv = collision(equipable1, equipable2) == false;
			if(!inv){
				throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
						+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
						+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
						+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
						+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
						+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
						+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
						+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
						+	" = false sinon");
			}
		}

		equipable1 = alex();
		equipable2 = slick();
		if( (equipable1.dimensions().largeur() + equipable2.dimensions().largeur())/2 <= (equipable1.position().x() - equipable2.position().x())
				|| (equipable1.dimensions().profondeur() + equipable2.dimensions().profondeur())/2 <= (equipable1.position().y() - equipable2.position().y())
				|| (equipable1.dimensions().hauteur() + equipable2.dimensions().hauteur())/2 <= (equipable1.position().z() - equipable2.position().z())
				){
			inv = collision(equipable1, equipable2) == true;
			if(!inv){
				throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
						+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
						+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
						+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
						+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
						+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
						+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
						+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
						+	" = false sinon");
			}
		}else{
			inv = collision(equipable1, equipable2) == false;
			if(!inv){
				throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
						+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
						+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
						+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
						+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
						+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
						+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
						+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
						+	" = false sinon");
			}
		}

		equipable1 = alex();
		equipable2 = slick();
		if( (equipable1.dimensions().largeur() + equipable2.dimensions().largeur())/2 <= (equipable1.position().x() - equipable2.position().x())
				|| (equipable1.dimensions().profondeur() + equipable2.dimensions().profondeur())/2 <= (equipable1.position().y() - equipable2.position().y())
				|| (equipable1.dimensions().hauteur() + equipable2.dimensions().hauteur())/2 <= (equipable1.position().z() - equipable2.position().z())
				){
			inv = collision(equipable1, equipable2) == true;
			if(!inv){
				throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
						+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
						+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
						+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
						+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
						+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
						+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
						+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
						+	" = false sinon");
			}
		}else{
			inv = collision(equipable1, equipable2) == false;
			if(!inv){
				throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
						+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
						+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
						+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
						+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
						+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
						+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
						+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
						+	" = false sinon");
			}
		}

		for(int i = 0; i < gangsters().size(); i++){
			equipable1 = alex();
			equipable2 = gangsters().get(i);
			if( (equipable1.dimensions().largeur() + equipable2.dimensions().largeur())/2 <= (equipable1.position().x() - equipable2.position().x())
					|| (equipable1.dimensions().profondeur() + equipable2.dimensions().profondeur())/2 <= (equipable1.position().y() - equipable2.position().y())
					|| (equipable1.dimensions().hauteur() + equipable2.dimensions().hauteur())/2 <= (equipable1.position().z() - equipable2.position().z())
					){
				inv = collision(equipable1, equipable2) == true;
				if(!inv){
					throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
							+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
							+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
							+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
							+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
							+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
							+	" = false sinon");
				}
			}else{
				inv = collision(equipable1, equipable2) == false;
				if(!inv){
					throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
							+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
							+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
							+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
							+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
							+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
							+	" = false sinon");
				}
			}
		}

		for(int i = 0; i < terrain().objets().size(); i++){
			equipable1 = alex();
			equipable2 =  terrain().objets().get(i);
			if( (equipable1.dimensions().largeur() + equipable2.dimensions().largeur())/2 <= (equipable1.position().x() - equipable2.position().x())
					|| (equipable1.dimensions().profondeur() + equipable2.dimensions().profondeur())/2 <= (equipable1.position().y() - equipable2.position().y())
					|| (equipable1.dimensions().hauteur() + equipable2.dimensions().hauteur())/2 <= (equipable1.position().z() - equipable2.position().z())
					){
				inv = collision(equipable1, equipable2) == true;
				if(!inv){
					throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
							+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
							+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
							+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
							+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
							+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
							+	" = false sinon");
				}
			}else{
				inv = collision(equipable1, equipable2) == false;
				if(!inv){
					throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
							+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
							+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
							+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
							+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
							+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
							+	" = false sinon");
				}
			}
		}

		equipable1 = ryan();
		equipable2 = slick();
		if( (equipable1.dimensions().largeur() + equipable2.dimensions().largeur())/2 <= (equipable1.position().x() - equipable2.position().x())
				|| (equipable1.dimensions().profondeur() + equipable2.dimensions().profondeur())/2 <= (equipable1.position().y() - equipable2.position().y())
				|| (equipable1.dimensions().hauteur() + equipable2.dimensions().hauteur())/2 <= (equipable1.position().z() - equipable2.position().z())
				){
			inv = collision(equipable1, equipable2) == true;
			if(!inv){
				throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
						+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
						+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
						+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
						+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
						+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
						+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
						+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
						+	" = false sinon");
			}
		}else{
			inv = collision(equipable1, equipable2) == false;
			if(!inv){
				throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
						+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
						+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
						+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
						+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
						+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
						+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
						+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
						+	" = false sinon");
			}
		}
		for(int i = 0; i < gangsters().size(); i++){
			equipable1 = ryan();
			equipable2 = gangsters().get(i);
			if( (equipable1.dimensions().largeur() + equipable2.dimensions().largeur())/2 <= (equipable1.position().x() - equipable2.position().x())
					|| (equipable1.dimensions().profondeur() + equipable2.dimensions().profondeur())/2 <= (equipable1.position().y() - equipable2.position().y())
					|| (equipable1.dimensions().hauteur() + equipable2.dimensions().hauteur())/2 <= (equipable1.position().z() - equipable2.position().z())
					){
				inv = collision(equipable1, equipable2) == true;
				if(!inv){
					throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
							+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
							+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
							+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
							+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
							+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
							+	" = false sinon");
				}
			}else{
				inv = collision(equipable1, equipable2) == false;
				if(!inv){
					throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
							+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
							+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
							+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
							+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
							+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
							+	" = false sinon");
				}
			}

		}

		for(int i = 0; i < terrain().objets().size(); i++){
			equipable1 = ryan();
			equipable2 =  terrain().objets().get(i);
			if( (equipable1.dimensions().largeur() + equipable2.dimensions().largeur())/2 <= (equipable1.position().x() - equipable2.position().x())
					|| (equipable1.dimensions().profondeur() + equipable2.dimensions().profondeur())/2 <= (equipable1.position().y() - equipable2.position().y())
					|| (equipable1.dimensions().hauteur() + equipable2.dimensions().hauteur())/2 <= (equipable1.position().z() - equipable2.position().z())
					){
				inv = collision(equipable1, equipable2) == true;
				if(!inv){
					throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
							+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
							+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
							+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
							+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
							+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
							+	" = false sinon");
				}
			}else{
				inv = collision(equipable1, equipable2) == false;
				if(!inv){
					throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
							+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
							+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
							+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
							+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
							+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
							+	" = false sinon");
				}
			}

		}


		for(int i = 0; i < gangsters().size(); i++){
			equipable1 = slick();
			equipable2 = gangsters().get(i);
			if( (equipable1.dimensions().largeur() + equipable2.dimensions().largeur())/2 <= (equipable1.position().x() - equipable2.position().x())
					|| (equipable1.dimensions().profondeur() + equipable2.dimensions().profondeur())/2 <= (equipable1.position().y() - equipable2.position().y())
					|| (equipable1.dimensions().hauteur() + equipable2.dimensions().hauteur())/2 <= (equipable1.position().z() - equipable2.position().z())
					){
				inv = collision(equipable1, equipable2) == true;
				if(!inv){
					throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
							+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
							+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
							+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
							+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
							+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
							+	" = false sinon");
				}
			}else{
				inv = collision(equipable1, equipable2) == false;
				if(!inv){
					throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
							+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
							+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
							+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
							+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
							+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
							+	" = false sinon");
				}
			}
		}

		for(int i = 0; i < terrain().objets().size(); i++){
			equipable1 = slick();
			equipable2 =  terrain().objets().get(i);
			if( (equipable1.dimensions().largeur() + equipable2.dimensions().largeur())/2 <= (equipable1.position().x() - equipable2.position().x())
					|| (equipable1.dimensions().profondeur() + equipable2.dimensions().profondeur())/2 <= (equipable1.position().y() - equipable2.position().y())
					|| (equipable1.dimensions().hauteur() + equipable2.dimensions().hauteur())/2 <= (equipable1.position().z() - equipable2.position().z())
					){
				inv = collision(equipable1, equipable2) == true;
				if(!inv){
					throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
							+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
							+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
							+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
							+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
							+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
							+	" = false sinon");
				}
			}else{
				inv = collision(equipable1, equipable2) == false;
				if(!inv){
					throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
							+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
							+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
							+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
							+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
							+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
							+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
							+	" = false sinon");
				}
			}
		}

		// gangsters
		for(int i = 0; i < gangsters().size(); i++){
			equipable1 = gangsters().get(i);
			for(int j = 0; j < gangsters().size(); j++){
				if(j!=i){
					equipable2 =  gangsters().get(j);

					if( (equipable1.dimensions().largeur() + equipable2.dimensions().largeur())/2 <= (equipable1.position().x() - equipable2.position().x())
							|| (equipable1.dimensions().profondeur() + equipable2.dimensions().profondeur())/2 <= (equipable1.position().y() - equipable2.position().y())
							|| (equipable1.dimensions().hauteur() + equipable2.dimensions().hauteur())/2 <= (equipable1.position().z() - equipable2.position().z())
							){
						inv = collision(equipable1, equipable2) == true;
						if(!inv){
							throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
									+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
									+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
									+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
									+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
									+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
									+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
									+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
									+	" = false sinon");
						}
					}else{
						inv = collision(equipable1, equipable2) == false;
						if(!inv){
							throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
									+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
									+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
									+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
									+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
									+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
									+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
									+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
									+	" = false sinon");
						}
					}
				}
			}
		}

		for(int i = 0; i < gangsters().size(); i++){
			equipable1 = gangsters().get(i);
			for(int j = 0; j < terrain().objets().size(); j++){
				equipable2 =  terrain().objets().get(j);
				if( (equipable1.dimensions().largeur() + equipable2.dimensions().largeur())/2 <= (equipable1.position().x() - equipable2.position().x())
						|| (equipable1.dimensions().profondeur() + equipable2.dimensions().profondeur())/2 <= (equipable1.position().y() - equipable2.position().y())
						|| (equipable1.dimensions().hauteur() + equipable2.dimensions().hauteur())/2 <= (equipable1.position().z() - equipable2.position().z())
						){
					inv = collision(equipable1, equipable2) == true;
					if(!inv){
						throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
								+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
								+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
								+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
								+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
								+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
								+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
								+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
								+	" = false sinon");
					}
				}else{
					inv = collision(equipable1, equipable2) == false;
					if(!inv){
						throw new InvariantError(" equipable1 appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))},"
								+ " * equipable2  appartient à {alex(), ryan(), slick(),  gangsters(), Terrain:objets(terrain(GC))} \\ equipable1"
								+ " collision(GC, equipable1, equipable2) = true si (Dimensions::largeur(Equipable::dimensions(equipable1)) - Dimensions::largeur(Equipable::dimensions(equipable2)) "
								+	"<= Position::x(Equipable::position(equipable1)) - Position::x(Equipable::position(equipable2))) ||"
								+	"(Dimensions::profondeur(Equipable::dimensions(equipable1)) - Dimensions::profondeur(Equipable::dimensions(equipable2)) "
								+	"<= Position::y(Equipable::position(equipable1)) - Position::y(Equipable::position(equipable2))) ||"
								+	"(Dimensions::hauteur(Equipable::dimensions(equipable1)) - Dimensions::hauteur(Equipable::dimensions(equipable2)) "
								+	"<= Position::z(Equipable::position(equipable1)) - Position::z(Equipable::position(equipable2))) ||"
								+	" = false sinon");
					}
				}
			}
		}




		/*
		 * personnage appartient à {alex(), ryan(), slick(),  gangsters()}
			collisionObjetLance(GC, personnage, objets) = O s'il existe un O appartenant à objets tel que collision(personnage, O) = true ^ Objet::estJete(O) != 0
												        = NULL s'il n'existe pas un O appartenant à objets tel que collision(personnage, O) = false ^ Objet::estJete(O) != 0
		 */

		List<Objet> objets = terrain().objets();

		Personnage personnage = alex();
		for(int i = 0; i < objets.size() ; i++){
			if(collision(personnage, objets.get(i)) && objets.get(i).estJete() != 0){
				inv = Toolbox.equals(collisionObjetRamasse(personnage, objets) ,objets.get(i));
				if(!inv) {
					throw new InvariantError(" personnage appartient à {alex(), ryan(), slick(),  gangsters()}"
							+ "collisionObjetLance(GC, personnage, objets) = O s'il existe un O appartenant à objets tel que collision(personnage, O) = true ^ Objet::estJete(O) != 0 "
							+ " = NULL s'il n'existe pas un O appartenant à objets tel que collision(personnage, O) = false ^ Objet::estJete(O) != 0");
				}
				break;
			}
		}

		personnage = ryan();
		for(int i = 0; i < objets.size() ; i++){
			if(collision(personnage, objets.get(i)) && objets.get(i).estJete() != 0){
				inv = Toolbox.equals(collisionObjetRamasse(personnage, objets) ,objets.get(i));
				if(!inv) {
					throw new InvariantError(" personnage appartient à {alex(), ryan(), slick(),  gangsters()}"
							+ "collisionObjetLance(GC, personnage, objets) = O s'il existe un O appartenant à objets tel que collision(personnage, O) = true ^ Objet::estJete(O) != 0 "
							+ " = NULL s'il n'existe pas un O appartenant à objets tel que collision(personnage, O) = false ^ Objet::estJete(O) != 0");
				}
				break;
			}
		}

		personnage = slick();
		for(int i = 0; i < objets.size() ; i++){
			if(collision(personnage, objets.get(i)) && objets.get(i).estJete() != 0){
				inv = Toolbox.equals(collisionObjetRamasse(personnage, objets) ,objets.get(i));
				if(!inv) {
					throw new InvariantError(" personnage appartient à {alex(), ryan(), slick(),  gangsters()}"
							+ "collisionObjetLance(GC, personnage, objets) = O s'il existe un O appartenant à objets tel que collision(personnage, O) = true ^ Objet::estJete(O) != 0 "
							+ " = NULL s'il n'existe pas un O appartenant à objets tel que collision(personnage, O) = false ^ Objet::estJete(O) != 0");
				}
				break;
			}
		}

		for(int j = 0; j < gangsters().size(); j++){
			personnage = gangsters().get(j);
			for(int i = 0; i < objets.size() ; i++){
				if(collision(personnage, objets.get(i)) && objets.get(i).estJete() != 0){
					inv = Toolbox.equals(collisionObjetRamasse(personnage, objets) ,objets.get(i));
					if(!inv) {
						throw new InvariantError(" personnage appartient à {alex(), ryan(), slick(),  gangsters()}"
								+ "collisionObjetLance(GC, personnage, objets) = O s'il existe un O appartenant à objets tel que collision(personnage, O) = true ^ Objet::estJete(O) != 0 "
								+ " = NULL s'il n'existe pas un O appartenant à objets tel que collision(personnage, O) = false ^ Objet::estJete(O) != 0");
					}
					break;
				}
			}
		}

		/*	collisionObjetRamasse(GC, personnage, objets) = O s'il existe un O appartenant à objets tel que collision(personnage, O) = true ^ Objet::estJete(O) = 0
        													= NULL s'il n'existe pas un O appartenant à objets tel que collision(personnage, O) = false ^ Objet::estJete(O) = 0
		 */
		
		objets = terrain().objets();

		personnage = alex();
		for(int i = 0; i < objets.size() ; i++){
			if(collision(personnage, objets.get(i)) && objets.get(i).estJete() == 0){
				inv = Toolbox.equals(collisionObjetRamasse(personnage, objets) ,objets.get(i));
				if(!inv) {
					throw new InvariantError(" personnage appartient à {alex(), ryan(), slick(),  gangsters()}"
							+ "collisionObjetLance(GC, personnage, objets) = O s'il existe un O appartenant à objets tel que collision(personnage, O) = true ^ Objet::estJete(O) != 0 "
							+ " = NULL s'il n'existe pas un O appartenant à objets tel que collision(personnage, O) = false ^ Objet::estJete(O) != 0");
				}
				break;
			}
		}

		personnage = ryan();
		for(int i = 0; i < objets.size() ; i++){
			if(collision(personnage, objets.get(i)) && objets.get(i).estJete() == 0){
				inv = Toolbox.equals(collisionObjetRamasse(personnage, objets) ,objets.get(i));
				if(!inv) {
					throw new InvariantError(" personnage appartient à {alex(), ryan(), slick(),  gangsters()}"
							+ "collisionObjetLance(GC, personnage, objets) = O s'il existe un O appartenant à objets tel que collision(personnage, O) = true ^ Objet::estJete(O) != 0 "
							+ " = NULL s'il n'existe pas un O appartenant à objets tel que collision(personnage, O) = false ^ Objet::estJete(O) != 0");
				}
				break;
			}
		}

		personnage = slick();
		for(int i = 0; i < objets.size() ; i++){
			if(collision(personnage, objets.get(i)) && objets.get(i).estJete() == 0){
				inv = Toolbox.equals(collisionObjetRamasse(personnage, objets) ,objets.get(i));
				if(!inv) {
					throw new InvariantError(" personnage appartient à {alex(), ryan(), slick(),  gangsters()}"
							+ "collisionObjetLance(GC, personnage, objets) = O s'il existe un O appartenant à objets tel que collision(personnage, O) = true ^ Objet::estJete(O) != 0 "
							+ " = NULL s'il n'existe pas un O appartenant à objets tel que collision(personnage, O) = false ^ Objet::estJete(O) != 0");
				}
				break;
			}
		}

		for(int j = 0; j < gangsters().size(); j++){
			personnage = gangsters().get(j);
			for(int i = 0; i < objets.size() ; i++){
				if(collision(personnage, objets.get(i)) && objets.get(i).estJete() == 0){
					inv = Toolbox.equals(collisionObjetRamasse(personnage, objets) ,objets.get(i));
					if(!inv) {
						throw new InvariantError(" personnage appartient à {alex(), ryan(), slick(),  gangsters()}"
								+ "collisionObjetLance(GC, personnage, objets) = O s'il existe un O appartenant à objets tel que collision(personnage, O) = true ^ Objet::estJete(O) != 0 "
								+ " = NULL s'il n'existe pas un O appartenant à objets tel que collision(personnage, O) = false ^ Objet::estJete(O) != 0");
					}
					break;
				}
			}
		}
	}
	
	
	
	/** _________________________________________________________ OBSERVATORS */
	
	@Override
	public Commande commandeAlex() {
		return super.commandeAlex();
	}

	@Override
	public Commande commandeRyan() {
		return super.commandeRyan();
	}
	@Override
	public Terrain terrain() {
		return super.terrain();
	}

	@Override
	public PersonnageJouable alex() {
		return super.alex();
	}

	@Override
	public PersonnageJouable ryan() {
		return super.ryan();
	}

	@Override
	public Gangster slick() {
		return super.slick();
	}

	@Override
	public List<Gangster> gangsters() {
		return super.gangsters();
	}

	@Override
	public boolean estPret() {
		return super.estPret();
	}

	@Override
	public boolean collision(Equipable equipable1, Equipable equipable2)
			throws ComposantError {
		return super.collision(equipable1, equipable2);
	}

	@Override
	public Objet collisionObjetLance(Personnage personnage, List<Objet> objets)
			throws ComposantError {
		return super.collisionObjetLance(personnage, objets);
	}

	@Override
	public Objet collisionObjetRamasse(Personnage personnage, List<Objet> objets)
			throws ComposantError {
		return super.collisionObjetRamasse(personnage, objets);
	}

	@Override
	public Personnage estFrappe(Personnage personnage) throws ComposantError {
		return super.estFrappe(personnage);
	}

	@Override
	public Personnage estPorte(Personnage personnage) throws ComposantError {
		return super.estPorte(personnage);
	}

	@Override
	public Commande commandesEnnemis() {
		return super.commandesEnnemis();
	}
	
	
	/** ________________________________________________________ CONSTRUCTORS */
	
	public void init(Terrain t) throws ComposantError{
		boolean pre;
		// pre init(t) require t != NULL
		
		pre = t != null;
		if(!pre) {
			throw new PreconditionError("init(t) require  t != NULL");
		}
		
		
		
		super.init(t);
		
		checkInvariants();
		
		boolean post;
		// post terrain(init(t)) = t
		post = Toolbox.equals(t, terrain()) == true;
		if(!post){
			throw new PostconditionError("post terrain(init(t)) = t");
		}
		
		// post commandeAlex(init(t)) = NULL
		post = commandeAlex() == null;
		if(!post){
			throw new PostconditionError("post commandeAlex(init(t)) = NULL");
		}
		
		// post commandeRyan(init(t)) = NULL
		post = commandeRyan() == null;
		if(!post){
			throw new PostconditionError("post commandeRyan(init(t)) = NULL");
		}
		// post alex(init(t)) = PersonnageJouable::init("Alex", Dimensions::init(10, 50, 10), 15, 100)
		PersonnageJouable alex_init = alex();
		Dimensions dimensionsalex_init = alex().dimensions();
		dimensionsalex_init.init(10, 50, 10);
		alex_init.init("alex", dimensionsalex_init , 15, 100);
		
		post = Toolbox.equals(alex_init, alex());
		if(!post){
			throw new PostconditionError("post alex(init(t)) = PersonnageJouable::init(\"Alex\", Dimensions::init(10, 50, 10), 15, 100)");
		}
		
		// post ryan(init(t)) = PersonnageJouable::init("Ryan", Dimensions::init(10, 50, 10), 15, 100)
		PersonnageJouable ryan_init = ryan();
		Dimensions dimensionsryan_init = ryan().dimensions();
		dimensionsryan_init.init(10, 50, 10);
		ryan_init.init("ryan", dimensionsryan_init , 15, 100);
		
		post = Toolbox.equals(ryan_init, ryan());
		if(!post){
			throw new PostconditionError("post ryan(init(t)) = PersonnageJouable::init(\"Ryan\", Dimensions::init(10, 50, 10), 15, 100)");
		}
		
		// post slick(init(t)) = Gangster::init("Slick", Dimensions::init(10, 50, 10), 15, 100)
		Gangster slick_init = slick();
		Dimensions dimensionsslick_init = slick().dimensions();
		dimensionsslick_init.init(10, 50, 10);
		slick_init.init("slick", dimensionsslick_init , 15, 100);
		post = Toolbox.equals(slick_init, slick());
		if(!post){
			throw new PostconditionError("post slick(init(t)) = Gangster::init(\"Slick\", Dimensions::init(10, 50, 10), 15, 100)");
		}
		
		
		// post gangsters(init(t)) = {Gangster::init("GenericDudes", Dimensions::init(10, 50, 10), 15, 100),
		//  						Gangster::init("HomeBoys", Dimensions::init(10, 50, 10), 15, 100),
		//  						Gangster::init("Squids", Dimensions::init(10, 50, 10), 15, 100),
		//  						Gangster::init("Squids2", Dimensions::init(10, 50, 10), 15, 100)}
		
		Gangster g1_init = gangsters().get(0);
		Dimensions dimensionsg1_init = gangsters().get(0).dimensions();
		dimensionsg1_init.init(10, 50, 10);
		g1_init.init("GenericDudes", dimensionsg1_init , 15, 100);
		
		Gangster g2_init = gangsters().get(1);
		Dimensions dimensionsg2_init = gangsters().get(1).dimensions();
		dimensionsg2_init.init(10, 50, 10);
		g2_init.init("HomeBoys", dimensionsg2_init , 15, 100);
		
		Gangster g3_init = gangsters().get(2);
		Dimensions dimensionsg3_init = gangsters().get(2).dimensions();
		dimensionsg3_init.init(10, 50, 10);
		g3_init.init("Squids", dimensionsg2_init , 15, 100);
		
		Gangster g4_init = gangsters().get(3);
		Dimensions dimensionsg4_init = gangsters().get(3).dimensions();
		dimensionsg4_init.init(10, 50, 10);
		g4_init.init("Squids2", dimensionsg2_init , 15, 100);
		
		List<Gangster> lg = new ArrayList<>();
		lg.add(g1_init);
		lg.add(g2_init);
		lg.add(g3_init);
		lg.add(g4_init);
		
		for(int i = 0; i < lg.size() ; i++){
			post = Toolbox.equals(lg.get(i), gangsters().get(i));
			if(!post){
				throw new PostconditionError("post gangsters(init(t)) = {Gangster::init(\"GenericDudes\", Dimensions::init(10, 50, 10), 15, 100),");
			}
		}
		
		// post estPret(init(t)) = false
		post = estPret() == false;
		if(!post){
			throw new PostconditionError("post estPret(init(t)) = false");
		}
		
		// post commandesEnnemis(init(t)) = null
		post = commandesEnnemis() == null;
		if(!post){
			throw new PostconditionError("post commandesEnnemis(init(t)) = null");
		}
		
		// post estFrappe(init(t),p) = NULL pour tout p appartenant à Personnage
		post = estFrappe(alex()) == null;
		if(!post){
			throw new PostconditionError("post estFrappe(init(t),p) = NULL pour tout p appartenant à Personnage");
		}
		
		// estPorte(init(t),p) = NULL pour tout p appartenant à Personnage
		post = estPorte(alex()) == null;
		if(!post){
			throw new PostconditionError("estPorte(init(t),p) = NULL pour tout p appartenant à Personnage");
		}
	}
	
	/** ___________________________________________________________ OPERATORS */
	
	
	public void gerer(Commande commande1, Commande commande2) throws ComposantError{
		boolean pre;
		// pre gerer(GC, commande1, commande2) require estPret(GC)
		pre = estPret();
		if(!pre){
			throw new PreconditionError("gerer(GC, commande1, commande2) require estPret(GC)");
		}
		
		boolean estPret_pre = estPret();
		PersonnageJouable alex_pre = alex();
		PersonnageJouable ryan_pre = ryan();
		Gangster slick_pre = slick();
		List<Gangster> lg_pre = gangsters();
		
		checkInvariants();
		
		super.gerer(commande1, commande2);
		
		checkInvariants();
		
		boolean post;
		// post estPret(gerer(GC, commande1,commande2)) = estPret(GC)
		post = estPret_pre == estPret();
		if(!post){
			throw new PostconditionError("estPret(gerer(GC, commande1,commande2)) = estPret(GC)");
		}
		
		// post commandeAlex(gerer(GC, commande1,commande2)) = commande1
		post = commandeAlex() == commande1;
		if(!post){
			throw new PostconditionError("commandeAlex(gerer(GC, commande1,commande2)) = commande1");
		}
		
		// post commandeRyan(gerer(GC, commande1,commande2)) = commande2
		post = commande2 == commandeRyan();
		if(!post){
			throw new PostconditionError("commandeRyan(gerer(GC, commande1,commande2)) = commande2");
		}
		
		// post alex(gerer(GC, commande1,commande2)) = alex(gererCommande(GC,alex(GC),commande1))
		gererCommande(alex_pre, commande1);
		post = Toolbox.equals(alex(), alex_pre);
		if(!post){
			throw new PostconditionError("alex(gerer(GC, commande1,commande2)) = alex(gererCommande(GC,alex(GC),commande1))");
		}
		
		// post ryan(gerer(GC, commande1,commande2)) = ryan(gererCommande(GC,ryan(GC),commande2))
		gererCommande(ryan_pre, commande2);
		post = Toolbox.equals(ryan(), ryan_pre);
		if(!post){
			throw new PostconditionError("ryan(gerer(GC, commande1,commande2)) = ryan(gererCommande(GC,ryan(GC),commande2))");
		}
		
		// post slick(gerer(GC, commande1,commande2)) = slick(gererCommande(GC,slick(GC), commandesEnnemis(GC)))
		gererCommande(slick_pre, commandesEnnemis());
		post = Toolbox.equals(slick(), slick_pre);
		if(!post){
			throw new PostconditionError("slick(gerer(GC, commande1,commande2)) = slick(gererCommande(GC,slick(GC), commandesEnnemis(GC)))");
		}
		
		// post gangsters(gerer(GC, commande1, commande2)) = pour tout g appartenant a gangsters
		//                                                  gererCommande(GC, g, commandesEnnemis(GC))
		for(int i =0; i < lg_pre.size(); i++){
			gererCommande(lg_pre.get(i), commandesEnnemis());
			post = Toolbox.equals(lg_pre.get(i), gangsters().get(i));
			if(!post){
				throw new PostconditionError(" gangsters(gerer(GC, commande1, commande2)) = pour tout g appartenant a gangsters"
						+ " gererCommande(GC, g, commandesEnnemis(GC))");
			}
		}
		// post  Terrain::objets(terrain(gerer(GC, commande1,commande2))) = impossible a spécifier aisement
	}
	
	
	public void avantPasJeu() throws ComposantError{
		boolean pre;
		// pre avantPasJeu(GC) require !estPret(GC)
		pre = estPret() == false;
		if(!pre){
			throw new PreconditionError("avantPasJeu(GC) require !estPret(GC)");
		}
		
		Terrain terrain_pre = terrain();
		PersonnageJouable alex_pre = alex();
		PersonnageJouable ryan_pre = ryan();
		Gangster slick_pre = slick();
		List<Gangster> gangsters_pre = gangsters();
		Commande commande_pre = commandesEnnemis();
		Commande commandeAlex_pre = commandeAlex();
		Commande commandeRyan_pre = commandeRyan();
		
		checkInvariants();
		
		super.avantPasJeu();
		
		checkInvariants();
		
		boolean post;
		
		// post commandeAlex(avantPasJeu(GC)) = commandeAlex(GC)
		post = commandeAlex() == commandeAlex_pre;
		if(!post){
			throw new PostconditionError("post commandeAlex(avantPasJeu(GC)) = commandeAlex(GC)");
		}
		
		// post commandeRyan(avantPasJeu(GC)) = commandeRyan(GC)
		post = commandeRyan() == commandeRyan_pre;
		if(!post){
			throw new PostconditionError("post commandeRyan(avantPasJeu(GC)) = commandeRyan(GC)");
		}
		
		/* post terrain(avantPasJeu(GC))  = terrain(GC) si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC)))) != BLOC_TYPE.FOSSE
													^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC)))) != BLOC_TYPE.FOSSE
											
											= Terrain::setBloc(Terrain::delBloc(terrain(GC), (Terrain::bloc(terrain(GC),Personnage::position(alex(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(alex(GC))))
											si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC)))) = BLOC_TYPE.FOSSE
											^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC)))) != BLOC_TYPE.FOSSE
											
											= Terrain::setBloc(Terrain::delBloc(terrain(GC), (Terrain::bloc(terrain(GC),Personnage::position(ryan(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(ryan(GC))))
											si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC)))) != BLOC_TYPE.FOSSE
											^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC)))) = BLOC_TYPE.FOSSE
											
											= Terrain::setBloc(Terrain::delBloc(Terrain::setBloc(Terrain::delBloc(terrain(GC), 
											(Terrain::bloc(terrain(GC),Personnage::position(alex(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(alex(GC))))
											, (Terrain::bloc(terrain(GC),Personnage::position(ryan(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(ryan(GC)))), 
											si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC))) = BLOC_TYPE.FOSSE
											^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC))) = BLOC_TYPE.FOSSE
											


*/
		if(terrain().bloc(alex().position()).type() != BlocType.FOSSE && terrain().bloc(ryan().position()).type() != BlocType.FOSSE){
			post = Toolbox.equals(terrain_pre, terrain());
			if(!post){
				throw new PostconditionError(" post terrain(avantPasJeu(GC))  = terrain(GC) si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC)))) != BLOC_TYPE.FOSSE "
											+ " ^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC)))) != BLOC_TYPE.FOSSE"
											+ " = Terrain::setBloc(Terrain::delBloc(terrain(GC), (Terrain::bloc(terrain(GC),Personnage::position(alex(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(alex(GC))))"
											+ " si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC)))) = BLOC_TYPE.FOSSE"
											+ " ^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC)))) != BLOC_TYPE.FOSSE"
											+ "= Terrain::setBloc(Terrain::delBloc(terrain(GC), (Terrain::bloc(terrain(GC),Personnage::position(ryan(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(ryan(GC))))"
											+ " si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC)))) != BLOC_TYPE.FOSSE"
											+ " ^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC)))) = BLOC_TYPE.FOSSE"
											+ " = Terrain::setBloc(Terrain::delBloc(Terrain::setBloc(Terrain::delBloc(terrain(GC), "
											+ " (Terrain::bloc(terrain(GC),Personnage::position(alex(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(alex(GC))))"
											+ " , (Terrain::bloc(terrain(GC),Personnage::position(ryan(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(ryan(GC)))),  "
											+ " , Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(ryan(GC))))"
											+ " si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC))) = BLOC_TYPE.FOSSE"
											+ " ^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC))) = BLOC_TYPE.FOSSE");
			}
		}
		if(terrain().bloc(alex().position()).type() == BlocType.FOSSE && terrain().bloc(ryan().position()).type() != BlocType.FOSSE){
			Bloc bloc = terrain().bloc(alex().position());
			terrain_pre.delBloc(terrain().bloc(alex().position()));
			bloc.init(BlocType.VIDE, alex().position());
			terrain_pre.setBloc(bloc);
			
			post = Toolbox.equals(terrain(), terrain_pre);
			if(!post){
				throw new PostconditionError(" post terrain(avantPasJeu(GC))  = terrain(GC) si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC)))) != BLOC_TYPE.FOSSE "
						+ " ^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC)))) != BLOC_TYPE.FOSSE"
						+ " = Terrain::setBloc(Terrain::delBloc(terrain(GC), (Terrain::bloc(terrain(GC),Personnage::position(alex(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(alex(GC))))"
						+ " si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC)))) = BLOC_TYPE.FOSSE"
						+ " ^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC)))) != BLOC_TYPE.FOSSE"
						+ "= Terrain::setBloc(Terrain::delBloc(terrain(GC), (Terrain::bloc(terrain(GC),Personnage::position(ryan(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(ryan(GC))))"
						+ " si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC)))) != BLOC_TYPE.FOSSE"
						+ " ^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC)))) = BLOC_TYPE.FOSSE"
						+ " = Terrain::setBloc(Terrain::delBloc(Terrain::setBloc(Terrain::delBloc(terrain(GC), "
						+ " (Terrain::bloc(terrain(GC),Personnage::position(alex(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(alex(GC))))"
						+ " , (Terrain::bloc(terrain(GC),Personnage::position(ryan(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(ryan(GC)))),  "
						+ " , Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(ryan(GC))))"
						+ " si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC))) = BLOC_TYPE.FOSSE"
						+ " ^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC))) = BLOC_TYPE.FOSSE");
			}
		}
		
		if(terrain().bloc(alex().position()).type() != BlocType.FOSSE && terrain().bloc(ryan().position()).type() == BlocType.FOSSE){
			Bloc bloc = terrain().bloc(ryan().position());
			terrain_pre.delBloc(terrain().bloc(ryan().position()));
			bloc.init(BlocType.VIDE, ryan().position());
			terrain_pre.setBloc(bloc);
			
			post = Toolbox.equals(terrain(), terrain_pre);
			if(!post){
				throw new PostconditionError(" post terrain(avantPasJeu(GC))  = terrain(GC) si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC)))) != BLOC_TYPE.FOSSE "
						+ " ^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC)))) != BLOC_TYPE.FOSSE"
						+ " = Terrain::setBloc(Terrain::delBloc(terrain(GC), (Terrain::bloc(terrain(GC),Personnage::position(alex(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(alex(GC))))"
						+ " si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC)))) = BLOC_TYPE.FOSSE"
						+ " ^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC)))) != BLOC_TYPE.FOSSE"
						+ "= Terrain::setBloc(Terrain::delBloc(terrain(GC), (Terrain::bloc(terrain(GC),Personnage::position(ryan(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(ryan(GC))))"
						+ " si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC)))) != BLOC_TYPE.FOSSE"
						+ " ^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC)))) = BLOC_TYPE.FOSSE"
						+ " = Terrain::setBloc(Terrain::delBloc(Terrain::setBloc(Terrain::delBloc(terrain(GC), "
						+ " (Terrain::bloc(terrain(GC),Personnage::position(alex(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(alex(GC))))"
						+ " , (Terrain::bloc(terrain(GC),Personnage::position(ryan(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(ryan(GC)))),  "
						+ " , Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(ryan(GC))))"
						+ " si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC))) = BLOC_TYPE.FOSSE"
						+ " ^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC))) = BLOC_TYPE.FOSSE");
			}
		}
		
		if(terrain().bloc(alex().position()).type() == BlocType.FOSSE && terrain().bloc(ryan().position()).type() == BlocType.FOSSE){
			Bloc bloc = terrain().bloc(ryan().position());
			terrain_pre.delBloc(terrain().bloc(ryan().position()));
			bloc.init(BlocType.VIDE, ryan().position());
			terrain_pre.setBloc(bloc);
			
			Bloc bloc2 = terrain().bloc(ryan().position());
			terrain_pre.delBloc(terrain().bloc(ryan().position()));
			bloc2.init(BlocType.VIDE, ryan().position());
			terrain_pre.setBloc(bloc2);
			
			post = Toolbox.equals(terrain(), terrain_pre);
			if(!post){
				throw new PostconditionError(" post terrain(avantPasJeu(GC))  = terrain(GC) si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC)))) != BLOC_TYPE.FOSSE "
						+ " ^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC)))) != BLOC_TYPE.FOSSE"
						+ " = Terrain::setBloc(Terrain::delBloc(terrain(GC), (Terrain::bloc(terrain(GC),Personnage::position(alex(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(alex(GC))))"
						+ " si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC)))) = BLOC_TYPE.FOSSE"
						+ " ^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC)))) != BLOC_TYPE.FOSSE"
						+ "= Terrain::setBloc(Terrain::delBloc(terrain(GC), (Terrain::bloc(terrain(GC),Personnage::position(ryan(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(ryan(GC))))"
						+ " si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC)))) != BLOC_TYPE.FOSSE"
						+ " ^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC)))) = BLOC_TYPE.FOSSE"
						+ " = Terrain::setBloc(Terrain::delBloc(Terrain::setBloc(Terrain::delBloc(terrain(GC), "
						+ " (Terrain::bloc(terrain(GC),Personnage::position(alex(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(alex(GC))))"
						+ " , (Terrain::bloc(terrain(GC),Personnage::position(ryan(GC))))), Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(ryan(GC)))),  "
						+ " , Bloc::init(BLOC_TYPE.VIDE, PersonnageJouable::position(ryan(GC))))"
						+ " si Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(alex(GC))) = BLOC_TYPE.FOSSE"
						+ " ^ Bloc::type(Terrain::bloc(terrain(GC),Personnage::position(ryan(GC))) = BLOC_TYPE.FOSSE");
			}
		}
		
		// post alex(avantPasJeu(GC)) = alex(GC)
		post = Toolbox.equals(alex(), alex_pre);
		if(!post){
			throw new PostconditionError("post alex(avantPasJeu(GC)) = alex(GC)");
		}
		
		// post ryan(avantPasJeu(GC)) = ryan(GC)
		post = Toolbox.equals(ryan(), ryan_pre);
		if(!post){
			throw new PostconditionError("post ryan(avantPasJeu(GC)) = ryan(GC)");
		}
		
		// post slick(avantPasJeu(GC)) = slick(GC)
		post = Toolbox.equals(slick(), slick_pre);
		if(!post){
			throw new PostconditionError("post slick(avantPasJeu(GC)) = slick(GC)");
		}
		
		// post gangsters(avantPasJeu(GC)) = gangsters(GC)
		post = Toolbox.equals(gangsters(), gangsters_pre);
		if(!post){
			throw new PostconditionError("post gangsters(avantPasJeu(GC)) = gangsters(GC))");
		}
		
		// post estPret(avantPasJeu(GC)) = true
		post = estPret();
		if(!post){
			throw new PostconditionError("post estPret(avantPasJeu(GC)) = true");
		}
		
		// post commandesEnnemis(avantPasJeu(GC)) = commandesEnnemis(GC)
		post = commande_pre == commandesEnnemis();
		if(!post){
			throw new PostconditionError("post commandesEnnemis(avantPasJeu(GC)) = commandesEnnemis(GC)");
		}
		/*		// post commandesEnnemis(gerer(GC, commande1,commande2)) = c appartenant à COMMANDE
		if (commandesEnnemis() == Commande.BAS || commandesEnnemis() == Commande.HAUT || commandesEnnemis() == Commande.GAUCHE ||
				commandesEnnemis() == Commande.DROITE || commandesEnnemis() == Commande.JETER  || commandesEnnemis() == Commande.RAMASSER ||
				commandesEnnemis() == Commande.FRAPPE ) {
			
		}else{
			throw new PostconditionError("post commandesEnnemis(gererCommande(GC, personnage,commande)) = c appartient COMMANDE");
		}
		*/
	}
	
	public void gererCommande(Personnage personnage, Commande commande) throws ComposantError{
		boolean pre;
		// pre gerer(GC, personnage, commande) require estPret(GC) ^ personnage != NULL
		pre = estPret() && !Toolbox.equals(personnage , null);
		if(!pre){
			throw new PreconditionError("gerer(GC, personnage, commande)  require estPret(GC) ^ personnage != NULL ^ commande != NULL");
		}
		
		
		boolean estPret_pre = estPret();
		Terrain terrain_pre = terrain();
		PersonnageJouable alex_pre = alex();
		PersonnageJouable ryan_pre = ryan();
		Gangster slick_pre = slick();
		List<Gangster> gangsters_pre = gangsters();
		Commande commandeAlex_pre = commandeAlex();
		Commande commandeRyan_pre = commandeRyan();

		checkInvariants();
		
		super.gererCommande(personnage, commande);;
		
		checkInvariants();
		
		boolean post;
		
		// post commandeAlex(gererCommande(GC, personnage,commande)) = commandeAlex(GC)
		post = commandeAlex_pre == commandeAlex();
		if(!post){
			throw new PostconditionError(" commandeAlex(gererCommande(GC, personnage,commande)) = commandeAlex(GC))");
		}
		
		// post commandeRyan(gererCommande(GC, personnage,commande)) = commandeRyan(GC))
		post = commandeRyan_pre == commandeRyan();
		if(!post){
			throw new PostconditionError(" commandeAlex(gererCommande(GC, personnage,commande)) = commandeAlex(GC))");
		}
		
		// post commandesEnnemis(gererCommande(GC, personnage,commande)) = c appartient COMMANDE
		if (commandesEnnemis() instanceof Commande) {
			
		}else{
			throw new PostconditionError("post commandesEnnemis(gererCommande(GC, personnage,commande)) = c appartient COMMANDE");
		}
		
		// post estPret(gererCommande(GC, personnage,commande)) = estPret(GC)
		post = estPret() == estPret_pre;
		if(!post){
			throw new PostconditionError("post estPret(gererCommande(GC, personnage,commande)) = estPret(GC)");
		}
		
		// post terrain(gererCommande(GC, personnage,commande)) = terrain(GC)
		post = Toolbox.equals(terrain(), terrain_pre);
		if(!post){
			throw new PostconditionError("post terrain(gererCommande(GC, personnage,commande)) = terrain(GC)");
		}
		
		/*post estPorte(gererCommande(GC, personnage,commande),alex(GC)) = g si pour tout g appartenant à {gansters(GC) U slick(GC)}
																	il existe un g tel que alex(GC) = Personnage::choseEquipee(g)
																  = NULL sinon
		*/
		if(Toolbox.equals(slick_pre.choseEquipee(),alex())){
			post = Toolbox.equals(estPorte(alex()), slick_pre);
			if(!post){
				throw new PostconditionError("post estPorte(gererCommande(GC, personnage,commande),alex(GC)) = g si pour tout g appartenant à {gansters(GC) U slick(GC)}"
						+ " il existe un g tel que alex(GC) = Personnage::choseEquipee(g)"
						+ " = NULL sinon");
			}
		}else{
			for(int i = 0; i < gangsters_pre.size() ; i++){
				if(Toolbox.equals(gangsters_pre.get(i).choseEquipee(),alex())){
					post =  Toolbox.equals(estPorte(alex()), gangsters_pre.get(i));
					if(!post){
						throw new PostconditionError("post estPorte(gererCommande(GC, personnage,commande),alex(GC)) = g si pour tout g appartenant à {gansters(GC) U slick(GC)}"
								+ " il existe un g tel que alex(GC) = Personnage::choseEquipee(g)"
								+ " = NULL sinon");
					}
				}
			}
			post = estPorte(alex()) == null;
			if(!post){
				throw new PostconditionError("post estPorte(gererCommande(GC, personnage,commande),alex(GC)) = g si pour tout g appartenant à {gansters(GC) U slick(GC)}"
						+ " il existe un g tel que alex(GC) = Personnage::choseEquipee(g)"
						+ " = NULL sinon");
			}
		}
		
		/*		estPorte(gererCommande(GC, personnage,commande),ryan(GC)) = g si pour tout g appartenant à {gansters(GC) U slick(GC)}
																	il existe un g tel que ryan(GC) = Personnage::choseEquipee(g)
																  = NULL sinon
		*/
		
		if(Toolbox.equals(slick_pre.choseEquipee(),ryan())){
			post = Toolbox.equals(estPorte(ryan()), slick_pre);
			if(!post){
				throw new PostconditionError("post estPorte(gererCommande(GC, personnage,commande),alex(GC)) = g si pour tout g appartenant à {gansters(GC) U slick(GC)}"
						+ " il existe un g tel que ryan(GC) = Personnage::choseEquipee(g)"
						+ " = NULL sinon");
			}
		}else{
			for(int i = 0; i < gangsters_pre.size() ; i++){
				if(Toolbox.equals(gangsters_pre.get(i).choseEquipee(),ryan())){
					post =  Toolbox.equals(estPorte(ryan()), gangsters_pre.get(i));
					if(!post){
						throw new PostconditionError("post estPorte(gererCommande(GC, personnage,commande),alex(GC)) = g si pour tout g appartenant à {gansters(GC) U slick(GC)}"
								+ " il existe un g tel que ryan(GC) = Personnage::choseEquipee(g)"
								+ " = NULL sinon");
					}
				}
			}
			post = estPorte(ryan()) == null;
			if(!post){
				throw new PostconditionError("post estPorte(gererCommande(GC, personnage,commande),alex(GC)) = g si pour tout g appartenant à {gansters(GC) U slick(GC)}"
						+ " il existe un g tel que ryan(GC) = Personnage::choseEquipee(g)"
						+ " = NULL sinon");
			}
		}
		
		
		/*		estPorte(gererCommande(GC, personnage,commande),g) =  p si pour tout p appartenant à {alex(GC), ryan(GC)}, g appartenant à {slick(GC), gansters(GC)}
															  il existe un p tel que g = Personnage::choseEquipee(p)
															  = NULL sinon
		*/
		
		if(Toolbox.equals(ryan_pre.choseEquipee(),slick())){
			post = Toolbox.equals(estPorte(slick()), ryan_pre);
			if(!post){
				throw new PostconditionError("post estPorte(gererCommande(GC, personnage,commande),g) =  p si pour tout p appartenant à {alex(GC), ryan(GC)}, g appartenant à {slick(GC), gansters(GC)}"
						+ "  il existe un p tel que g = Personnage::choseEquipee(p)"
						+ " = NULL sinon");
			}
		}else{
			if(Toolbox.equals(alex_pre.choseEquipee(),slick())){
				post = Toolbox.equals(estPorte(slick()), alex_pre);
				if(!post){
					throw new PostconditionError("post estPorte(gererCommande(GC, personnage,commande),g) =  p si pour tout p appartenant à {alex(GC), ryan(GC)}, g appartenant à {slick(GC), gansters(GC)}"
							+ "  il existe un p tel que g = Personnage::choseEquipee(p)"
							+ " = NULL sinon");
				}else{
					post =  estPorte(slick()) == null;
					if(!post){
						throw new PostconditionError("post estPorte(gererCommande(GC, personnage,commande),g) =  p si pour tout p appartenant à {alex(GC), ryan(GC)}, g appartenant à {slick(GC), gansters(GC)}"
								+ "  il existe un p tel que g = Personnage::choseEquipee(p)"
								+ " = NULL sinon");
					}
				}
			}
		}
		/*		estFrappe(gererCommande(GC, personnage,commande),alex(GC)) = g si pour tout g appartenant à {gansters(GC) U slick(GC)},commandesEnnemis(GC) = COMMANDE.FRAPPE
																     il existe un g tel que collision(g,alex(GC)) = true
																   = NULL sinon	
		*/
		
		if(commandesEnnemis() == Commande.FRAPPE){
			if(collision(alex_pre, slick_pre)){
				post =  Toolbox.equals(estFrappe(alex_pre), slick_pre);
				if(!post){
					throw new PostconditionError("post estPorte(gererCommande(GC, personnage,commande),g) =  p si pour tout p appartenant à {alex(GC), ryan(GC)}, g appartenant à {slick(GC), gansters(GC)}"
							+ "  il existe un p tel que g = Personnage::choseEquipee(p)"
							+ " = NULL sinon");
				}
			}
		}
		// TODO : finir les estfrappe...
		
		
		
		
		
		Personnage p = alex_pre;
		
		
		if(Toolbox.equals(p, personnage) || (estFrappe(p) == null && p.estGele() == 0 && commande == null )){
			post = Toolbox.equals(p, alex());
			if(!post){
				throw new PostconditionError("		alex(gererCommande(GC, personnage,commande)) = alex(GC) si personnage != alex(GC) || (estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele(alex(GC)) ^ commande = NULL)"
											+		" = PersonnageJouable::deplacer(alex(GC), Position::init(max(Position::x(alex(GC)) -1, 0)), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) "
											+		" = PersonnageJouable::deplacer(alex(GC), Position::init(min(Position::x(alex(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC))"
											+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), max(Position::y(alex(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele(alex(GC))"
											+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), min(Position::y(alex(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele( alex(GC))"
											+		" = PersonnageJouable::deplacer(alex(GC), Personnage::position(estPorte(GC, alex(GC)))) si estPorte(GC, alex(GC)) != NULL"
											+		" = PersonnageJouable::jeter(alex(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, alex(GC)) != NULL ^ !Personnage::estGele( alex(GC))"	 
											+		" = PersonnageJouable::ramasser(alex(GC), collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) ^"
											+		" collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC)) != NULL"
											+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Personnage::force(estFrappe(GC, alex(GC)))), 5) si estFrappe(GC, alex(GC)) != NULL "
											+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Objet::bonusDeForce(collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))) != NULL"
											+       " = Personnage::geler(alex(GC), 5) si personnage = alex(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(alex(GC))"
											+		" = Personnage::degeler() sinon");
			}
		}
		
		
		
		if(Toolbox.equals(p, personnage) || (estFrappe(p) == null && p.estGele() == 0 && commande == null )){
			post = Toolbox.equals(p, alex());
			if(!post){
				throw new PostconditionError("		alex(gererCommande(GC, personnage,commande)) = alex(GC) si personnage != alex(GC) || (estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele(alex(GC)) ^ commande = NULL)"
											+		" = PersonnageJouable::deplacer(alex(GC), Position::init(max(Position::x(alex(GC)) -1, 0)), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) "
											+		" = PersonnageJouable::deplacer(alex(GC), Position::init(min(Position::x(alex(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC))"
											+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), max(Position::y(alex(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele(alex(GC))"
											+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), min(Position::y(alex(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele( alex(GC))"
											+		" = PersonnageJouable::deplacer(alex(GC), Personnage::position(estPorte(GC, alex(GC)))) si estPorte(GC, alex(GC)) != NULL"
											+		" = PersonnageJouable::jeter(alex(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, alex(GC)) != NULL ^ !Personnage::estGele( alex(GC))"	 
											+		" = PersonnageJouable::ramasser(alex(GC), collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) ^"
											+		" collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC)) != NULL"
											+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Personnage::force(estFrappe(GC, alex(GC)))), 5) si estFrappe(GC, alex(GC)) != NULL "
											+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Objet::bonusDeForce(collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))) != NULL"
											+       " = Personnage::geler(alex(GC), 5) si personnage = alex(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(alex(GC))"
											+		" = Personnage::degeler() sinon");
			}
		}
		
		if(commande == Commande.GAUCHE && estFrappe(p) == null && p.estGele() == 0 && Toolbox.equals(personnage,p)){
			p.position().init(Math.max(p.position().x() -1,0) , p.position().y(), p.position().z());
			p.deplacer(p.position());
			post = Toolbox.equals(p, alex());
			if(!post){
				throw new PostconditionError("		alex(gererCommande(GC, personnage,commande)) = alex(GC) si personnage != alex(GC) || (estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele(alex(GC)) ^ commande = NULL)"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(max(Position::x(alex(GC)) -1, 0)), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) "
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(min(Position::x(alex(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), max(Position::y(alex(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele(alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), min(Position::y(alex(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Personnage::position(estPorte(GC, alex(GC)))) si estPorte(GC, alex(GC)) != NULL"
						+		" = PersonnageJouable::jeter(alex(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, alex(GC)) != NULL ^ !Personnage::estGele( alex(GC))"	 
						+		" = PersonnageJouable::ramasser(alex(GC), collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) ^"
						+		" collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC)) != NULL"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Personnage::force(estFrappe(GC, alex(GC)))), 5) si estFrappe(GC, alex(GC)) != NULL "
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Objet::bonusDeForce(collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))) != NULL"
						+       " = Personnage::geler(alex(GC), 5) si personnage = alex(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(alex(GC))"
						+		" = Personnage::degeler() sinon");
			}
		}
		
		if(commande == Commande.DROITE && estFrappe(p) == null && p.estGele() == 0 && Toolbox.equals(personnage,p)){
			p.position().init(Math.max(p.position().x() +1, terrain().dimensions().largeur()) , p.position().y(), p.position().z());
			p.deplacer(p.position());
			post = Toolbox.equals(p, alex());
			if(!post){
				throw new PostconditionError("		alex(gererCommande(GC, personnage,commande)) = alex(GC) si personnage != alex(GC) || (estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele(alex(GC)) ^ commande = NULL)"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(max(Position::x(alex(GC)) -1, 0)), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) "
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(min(Position::x(alex(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), max(Position::y(alex(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele(alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), min(Position::y(alex(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Personnage::position(estPorte(GC, alex(GC)))) si estPorte(GC, alex(GC)) != NULL"
						+		" = PersonnageJouable::jeter(alex(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, alex(GC)) != NULL ^ !Personnage::estGele( alex(GC))"	 
						+		" = PersonnageJouable::ramasser(alex(GC), collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) ^"
						+		" collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC)) != NULL"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Personnage::force(estFrappe(GC, alex(GC)))), 5) si estFrappe(GC, alex(GC)) != NULL "
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Objet::bonusDeForce(collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))) != NULL"
						+       " = Personnage::geler(alex(GC), 5) si personnage = alex(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(alex(GC))"
						+		" = Personnage::degeler() sinon");
			}
		}
		
		if(commande == Commande.HAUT && estFrappe(p) == null && p.estGele() == 0 && Toolbox.equals(personnage,p)){
			p.position().init(p.position().x() ,Math.min( p.position().y() +1 , terrain().dimensions().profondeur()), p.position().z());
			p.deplacer(p.position());
			post = Toolbox.equals(p, alex());
			if(!post){
				throw new PostconditionError("		alex(gererCommande(GC, personnage,commande)) = alex(GC) si personnage != alex(GC) || (estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele(alex(GC)) ^ commande = NULL)"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(max(Position::x(alex(GC)) -1, 0)), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) "
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(min(Position::x(alex(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), max(Position::y(alex(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele(alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), min(Position::y(alex(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Personnage::position(estPorte(GC, alex(GC)))) si estPorte(GC, alex(GC)) != NULL"
						+		" = PersonnageJouable::jeter(alex(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, alex(GC)) != NULL ^ !Personnage::estGele( alex(GC))"	 
						+		" = PersonnageJouable::ramasser(alex(GC), collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) ^"
						+		" collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC)) != NULL"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Personnage::force(estFrappe(GC, alex(GC)))), 5) si estFrappe(GC, alex(GC)) != NULL "
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Objet::bonusDeForce(collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))) != NULL"
						+       " = Personnage::geler(alex(GC), 5) si personnage = alex(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(alex(GC))"
						+		" = Personnage::degeler() sinon");
			}
		}
		
		if(commande == Commande.BAS && estFrappe(p) == null && p.estGele() == 0 && Toolbox.equals(personnage,p)){
			p.position().init(p.position().x() ,Math.max( p.position().y() -1, terrain().dimensions().profondeur()), p.position().z());
			p.deplacer(p.position());
			post = Toolbox.equals(p, alex());
			if(!post){
				throw new PostconditionError("		alex(gererCommande(GC, personnage,commande)) = alex(GC) si personnage != alex(GC) || (estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele(alex(GC)) ^ commande = NULL)"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(max(Position::x(alex(GC)) -1, 0)), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) "
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(min(Position::x(alex(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), max(Position::y(alex(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele(alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), min(Position::y(alex(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Personnage::position(estPorte(GC, alex(GC)))) si estPorte(GC, alex(GC)) != NULL"
						+		" = PersonnageJouable::jeter(alex(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, alex(GC)) != NULL ^ !Personnage::estGele( alex(GC))"	 
						+		" = PersonnageJouable::ramasser(alex(GC), collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) ^"
						+		" collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC)) != NULL"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Personnage::force(estFrappe(GC, alex(GC)))), 5) si estFrappe(GC, alex(GC)) != NULL "
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Objet::bonusDeForce(collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))) != NULL"
						+       " = Personnage::geler(alex(GC), 5) si personnage = alex(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(alex(GC))"
						+		" = Personnage::degeler() sinon");
			}
		}
		
		if(commande == Commande.JETER && estFrappe(p)!=null && p.estGele() == 0 && Toolbox.equals(personnage,p)){
			p.jeter();
			post = Toolbox.equals(p, alex());
			if(!post){
				throw new PostconditionError("		alex(gererCommande(GC, personnage,commande)) = alex(GC) si personnage != alex(GC) || (estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele(alex(GC)) ^ commande = NULL)"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(max(Position::x(alex(GC)) -1, 0)), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) "
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(min(Position::x(alex(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), max(Position::y(alex(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele(alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), min(Position::y(alex(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Personnage::position(estPorte(GC, alex(GC)))) si estPorte(GC, alex(GC)) != NULL"
						+		" = PersonnageJouable::jeter(alex(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, alex(GC)) != NULL ^ !Personnage::estGele( alex(GC))"	 
						+		" = PersonnageJouable::ramasser(alex(GC), collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) ^"
						+		" collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC)) != NULL"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Personnage::force(estFrappe(GC, alex(GC)))), 5) si estFrappe(GC, alex(GC)) != NULL "
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Objet::bonusDeForce(collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))) != NULL"
						+       " = Personnage::geler(alex(GC), 5) si personnage = alex(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(alex(GC))"
						+		" = Personnage::degeler() sinon");
			}
		}
		
		if(commande == Commande.RAMASSER && estFrappe(p)!=null && p.estGele() == 0 && Toolbox.equals(personnage,p) && collisionObjetRamasse(p, terrain_pre.objets()) != null){
			p.ramasser(collisionObjetRamasse(p, terrain_pre.objets()));
			post = Toolbox.equals(p, alex());
			if(!post){
				throw new PostconditionError("		alex(gererCommande(GC, personnage,commande)) = alex(GC) si personnage != alex(GC) || (estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele(alex(GC)) ^ commande = NULL)"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(max(Position::x(alex(GC)) -1, 0)), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) "
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(min(Position::x(alex(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), max(Position::y(alex(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele(alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), min(Position::y(alex(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Personnage::position(estPorte(GC, alex(GC)))) si estPorte(GC, alex(GC)) != NULL"
						+		" = PersonnageJouable::jeter(alex(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, alex(GC)) != NULL ^ !Personnage::estGele( alex(GC))"	 
						+		" = PersonnageJouable::ramasser(alex(GC), collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) ^"
						+		" collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC)) != NULL"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Personnage::force(estFrappe(GC, alex(GC)))), 5) si estFrappe(GC, alex(GC)) != NULL "
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Objet::bonusDeForce(collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))) != NULL"
						+       " = Personnage::geler(alex(GC), 5) si personnage = alex(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(alex(GC))"
						+		" = Personnage::degeler() sinon");
			}
		}
		
		if(estFrappe(p)!= null && Toolbox.equals(p, personnage)){
			p.retirerPointsDeVie(estFrappe(p).force());
			p.geler(5);
			post = Toolbox.equals(p, alex());
			if(!post){
				throw new PostconditionError("		alex(gererCommande(GC, personnage,commande)) = alex(GC) si personnage != alex(GC) || (estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele(alex(GC)) ^ commande = NULL)"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(max(Position::x(alex(GC)) -1, 0)), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) "
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(min(Position::x(alex(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), max(Position::y(alex(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele(alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), min(Position::y(alex(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Personnage::position(estPorte(GC, alex(GC)))) si estPorte(GC, alex(GC)) != NULL"
						+		" = PersonnageJouable::jeter(alex(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, alex(GC)) != NULL ^ !Personnage::estGele( alex(GC))"	 
						+		" = PersonnageJouable::ramasser(alex(GC), collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) ^"
						+		" collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC)) != NULL"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Personnage::force(estFrappe(GC, alex(GC)))), 5) si estFrappe(GC, alex(GC)) != NULL "
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Objet::bonusDeForce(collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))) != NULL"
						+       " = Personnage::geler(alex(GC), 5) si personnage = alex(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(alex(GC))"
						+		" = Personnage::degeler() sinon");
			}
		}
		
		if(Toolbox.equals(p, personnage) && collisionObjetLance(p, terrain_pre.objets()) != null){
			p.retirerPointsDeVie(collisionObjetLance(p, terrain_pre.objets()).bonusDeForce());
			p.geler(5);
			post = Toolbox.equals(p, alex());
			if(!post){
				throw new PostconditionError("		alex(gererCommande(GC, personnage,commande)) = alex(GC) si personnage != alex(GC) || (estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele(alex(GC)) ^ commande = NULL)"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(max(Position::x(alex(GC)) -1, 0)), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) "
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(min(Position::x(alex(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), max(Position::y(alex(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele(alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), min(Position::y(alex(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Personnage::position(estPorte(GC, alex(GC)))) si estPorte(GC, alex(GC)) != NULL"
						+		" = PersonnageJouable::jeter(alex(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, alex(GC)) != NULL ^ !Personnage::estGele( alex(GC))"	 
						+		" = PersonnageJouable::ramasser(alex(GC), collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) ^"
						+		" collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC)) != NULL"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Personnage::force(estFrappe(GC, alex(GC)))), 5) si estFrappe(GC, alex(GC)) != NULL "
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Objet::bonusDeForce(collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))) != NULL"
						+       " = Personnage::geler(alex(GC), 5) si personnage = alex(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(alex(GC))"
						+		" = Personnage::degeler() sinon");
			}
		}
		if(Toolbox.equals(p, personnage)){
			p.degeler();
			post = Toolbox.equals(p, alex());
			if(!post){
				throw new PostconditionError("		alex(gererCommande(GC, personnage,commande)) = alex(GC) si personnage != alex(GC) || (estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele(alex(GC)) ^ commande = NULL)"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(max(Position::x(alex(GC)) -1, 0)), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) "
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(min(Position::x(alex(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(alex(GC)), Position::z(alex(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), max(Position::y(alex(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele(alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Position::init(Position::x(alex(GC)), min(Position::y(alex(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, alex(GC)) = NULL  ^ !Personnage::estGele( alex(GC))"
						+		" = PersonnageJouable::deplacer(alex(GC), Personnage::position(estPorte(GC, alex(GC)))) si estPorte(GC, alex(GC)) != NULL"
						+		" = PersonnageJouable::jeter(alex(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, alex(GC)) != NULL ^ !Personnage::estGele( alex(GC))"	 
						+		" = PersonnageJouable::ramasser(alex(GC), collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, alex(GC)) = NULL ^ !Personnage::estGele( alex(GC)) ^"
						+		" collisionObjetRamasse(GC, alex(GC), Terrain::objets(terrain(GC)) != NULL"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Personnage::force(estFrappe(GC, alex(GC)))), 5) si estFrappe(GC, alex(GC)) != NULL "
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(alex(GC), Objet::bonusDeForce(collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,alex(GC),Terrain::objets(terrain(GC))) != NULL"
						+       " = Personnage::geler(alex(GC), 5) si personnage = alex(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(alex(GC))"
						+		" = Personnage::degeler() sinon");
			}
		}
		
		//ryan
		
		p = ryan_pre;
		
		if(Toolbox.equals(p, personnage) || (estFrappe(p) == null && p.estGele() == 0 && commande == null )){
			post = Toolbox.equals(p, ryan());
			if(!post){
				throw new PostconditionError("		ryan(gererCommande(GC, personnage,commande)) = ryan(GC) si personnage != ryan(GC) || estFrappe(GC, ryan(GC)) = NULL ^ Personnage::estGele( ryan(GC)) ^ commande = NULL "
											+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(max(Position::x(ryan(GC)) -1, 0)), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC) ^ personnage = ryan(GC)"
											+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(min(Position::x(ryan(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele(ryan(GC)) ^ personnage = ryan(GC))"
											+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), min(Position::y(ryan(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
											+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), max(Position::y(ryan(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
											+		" = PersonnageJouable::deplacer(ryan(GC), Personnage::position(estPorte(GC, ryan(GC)))) si estPorte(GC, ryan(GC)) != NULL"
											+		" = PersonnageJouable::jeter(ryan(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, ryan(GC)) != NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"	 
											+		" = PersonnageJouable::ramasser(ryan(GC), collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^"
											+		" collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC)) != NULL ^ personnage = ryan(GC)"
											+		"  = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Personnage::force(estFrappe(GC, ryan(GC)))), 5) si estFrappe(GC, ryan(GC)) != NULL ^ personnage = ryan(GC)"
											+		" = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Objet::bonusDeForce(collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))) != NULL ^ personnage = ryan(GC)"
											+       " = Personnage::geler(ryan(GC), 5) si personnage = ryan(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(ryan(GC))"
											+		" = Personnage::degeler() sinon");
			}
		}
		
		if(commande == Commande.GAUCHE && estFrappe(p) == null && p.estGele() == 0 && Toolbox.equals(personnage,p)){
			p.position().init(Math.max(p.position().x() -1,0) , p.position().y(), p.position().z());
			p.deplacer(p.position());
			post = Toolbox.equals(p, ryan());
			if(!post){
				throw new PostconditionError("		ryan(gererCommande(GC, personnage,commande)) = ryan(GC) si personnage != ryan(GC) || estFrappe(GC, ryan(GC)) = NULL ^ Personnage::estGele( ryan(GC)) ^ commande = NULL "
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(max(Position::x(ryan(GC)) -1, 0)), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(min(Position::x(ryan(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele(ryan(GC)) ^ personnage = ryan(GC))"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), min(Position::y(ryan(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), max(Position::y(ryan(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Personnage::position(estPorte(GC, ryan(GC)))) si estPorte(GC, ryan(GC)) != NULL"
						+		" = PersonnageJouable::jeter(ryan(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, ryan(GC)) != NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"	 
						+		" = PersonnageJouable::ramasser(ryan(GC), collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^"
						+		" collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC)) != NULL ^ personnage = ryan(GC)"
						+		"  = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Personnage::force(estFrappe(GC, ryan(GC)))), 5) si estFrappe(GC, ryan(GC)) != NULL ^ personnage = ryan(GC)"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Objet::bonusDeForce(collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))) != NULL ^ personnage = ryan(GC)"
						+       " = Personnage::geler(ryan(GC), 5) si personnage = ryan(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(ryan(GC))"
						+		" = Personnage::degeler() sinon");
}
		}
		
		if(commande == Commande.DROITE && estFrappe(p) == null && p.estGele() == 0 && Toolbox.equals(personnage,p)){
			p.position().init(Math.max(p.position().x() +1, terrain().dimensions().largeur()) , p.position().y(), p.position().z());
			p.deplacer(p.position());
			post = Toolbox.equals(p, ryan());
			if(!post){
				throw new PostconditionError("		ryan(gererCommande(GC, personnage,commande)) = ryan(GC) si personnage != ryan(GC) || estFrappe(GC, ryan(GC)) = NULL ^ Personnage::estGele( ryan(GC)) ^ commande = NULL "
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(max(Position::x(ryan(GC)) -1, 0)), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(min(Position::x(ryan(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele(ryan(GC)) ^ personnage = ryan(GC))"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), min(Position::y(ryan(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), max(Position::y(ryan(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Personnage::position(estPorte(GC, ryan(GC)))) si estPorte(GC, ryan(GC)) != NULL"
						+		" = PersonnageJouable::jeter(ryan(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, ryan(GC)) != NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"	 
						+		" = PersonnageJouable::ramasser(ryan(GC), collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^"
						+		" collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC)) != NULL ^ personnage = ryan(GC)"
						+		"  = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Personnage::force(estFrappe(GC, ryan(GC)))), 5) si estFrappe(GC, ryan(GC)) != NULL ^ personnage = ryan(GC)"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Objet::bonusDeForce(collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))) != NULL ^ personnage = ryan(GC)"
						+       " = Personnage::geler(ryan(GC), 5) si personnage = ryan(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(ryan(GC))"
						+		" = Personnage::degeler() sinon");
}
		}
		
		if(commande == Commande.HAUT && estFrappe(p) == null && p.estGele() == 0 && Toolbox.equals(personnage,p)){
			p.position().init(p.position().x() ,Math.min( p.position().y() +1 , terrain().dimensions().profondeur()), p.position().z());
			p.deplacer(p.position());
			post = Toolbox.equals(p, ryan());
			if(!post){
				throw new PostconditionError("		ryan(gererCommande(GC, personnage,commande)) = ryan(GC) si personnage != ryan(GC) || estFrappe(GC, ryan(GC)) = NULL ^ Personnage::estGele( ryan(GC)) ^ commande = NULL "
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(max(Position::x(ryan(GC)) -1, 0)), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(min(Position::x(ryan(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele(ryan(GC)) ^ personnage = ryan(GC))"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), min(Position::y(ryan(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), max(Position::y(ryan(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Personnage::position(estPorte(GC, ryan(GC)))) si estPorte(GC, ryan(GC)) != NULL"
						+		" = PersonnageJouable::jeter(ryan(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, ryan(GC)) != NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"	 
						+		" = PersonnageJouable::ramasser(ryan(GC), collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^"
						+		" collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC)) != NULL ^ personnage = ryan(GC)"
						+		"  = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Personnage::force(estFrappe(GC, ryan(GC)))), 5) si estFrappe(GC, ryan(GC)) != NULL ^ personnage = ryan(GC)"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Objet::bonusDeForce(collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))) != NULL ^ personnage = ryan(GC)"
						+       " = Personnage::geler(ryan(GC), 5) si personnage = ryan(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(ryan(GC))"
						+		" = Personnage::degeler() sinon");
}
		}
		
		if(commande == Commande.BAS && estFrappe(p) == null && p.estGele() == 0 && Toolbox.equals(personnage,p)){
			p.position().init(p.position().x() ,Math.max( p.position().y() -1, terrain().dimensions().profondeur()), p.position().z());
			p.deplacer(p.position());
			post = Toolbox.equals(p, ryan());
			if(!post){
				throw new PostconditionError("		ryan(gererCommande(GC, personnage,commande)) = ryan(GC) si personnage != ryan(GC) || estFrappe(GC, ryan(GC)) = NULL ^ Personnage::estGele( ryan(GC)) ^ commande = NULL "
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(max(Position::x(ryan(GC)) -1, 0)), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(min(Position::x(ryan(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele(ryan(GC)) ^ personnage = ryan(GC))"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), min(Position::y(ryan(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), max(Position::y(ryan(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Personnage::position(estPorte(GC, ryan(GC)))) si estPorte(GC, ryan(GC)) != NULL"
						+		" = PersonnageJouable::jeter(ryan(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, ryan(GC)) != NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"	 
						+		" = PersonnageJouable::ramasser(ryan(GC), collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^"
						+		" collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC)) != NULL ^ personnage = ryan(GC)"
						+		"  = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Personnage::force(estFrappe(GC, ryan(GC)))), 5) si estFrappe(GC, ryan(GC)) != NULL ^ personnage = ryan(GC)"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Objet::bonusDeForce(collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))) != NULL ^ personnage = ryan(GC)"
						+       " = Personnage::geler(ryan(GC), 5) si personnage = ryan(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(ryan(GC))"
						+		" = Personnage::degeler() sinon");
}
		}
		
		if(commande == Commande.JETER && estFrappe(p)!=null && p.estGele() == 0 && Toolbox.equals(personnage,p)){
			p.jeter();
			post = Toolbox.equals(p, ryan());
			if(!post){
				throw new PostconditionError("		ryan(gererCommande(GC, personnage,commande)) = ryan(GC) si personnage != ryan(GC) || estFrappe(GC, ryan(GC)) = NULL ^ Personnage::estGele( ryan(GC)) ^ commande = NULL "
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(max(Position::x(ryan(GC)) -1, 0)), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(min(Position::x(ryan(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele(ryan(GC)) ^ personnage = ryan(GC))"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), min(Position::y(ryan(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), max(Position::y(ryan(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Personnage::position(estPorte(GC, ryan(GC)))) si estPorte(GC, ryan(GC)) != NULL"
						+		" = PersonnageJouable::jeter(ryan(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, ryan(GC)) != NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"	 
						+		" = PersonnageJouable::ramasser(ryan(GC), collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^"
						+		" collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC)) != NULL ^ personnage = ryan(GC)"
						+		"  = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Personnage::force(estFrappe(GC, ryan(GC)))), 5) si estFrappe(GC, ryan(GC)) != NULL ^ personnage = ryan(GC)"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Objet::bonusDeForce(collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))) != NULL ^ personnage = ryan(GC)"
						+       " = Personnage::geler(ryan(GC), 5) si personnage = ryan(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(ryan(GC))"
						+		" = Personnage::degeler() sinon");
}
		}
		
		if(commande == Commande.RAMASSER && estFrappe(p)!=null && p.estGele() == 0 && Toolbox.equals(personnage,p) && collisionObjetRamasse(p, terrain_pre.objets()) != null){
			p.ramasser(collisionObjetRamasse(p, terrain_pre.objets()));
			post = Toolbox.equals(p, ryan());
			if(!post){
				throw new PostconditionError("		ryan(gererCommande(GC, personnage,commande)) = ryan(GC) si personnage != ryan(GC) || estFrappe(GC, ryan(GC)) = NULL ^ Personnage::estGele( ryan(GC)) ^ commande = NULL "
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(max(Position::x(ryan(GC)) -1, 0)), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(min(Position::x(ryan(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele(ryan(GC)) ^ personnage = ryan(GC))"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), min(Position::y(ryan(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), max(Position::y(ryan(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Personnage::position(estPorte(GC, ryan(GC)))) si estPorte(GC, ryan(GC)) != NULL"
						+		" = PersonnageJouable::jeter(ryan(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, ryan(GC)) != NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"	 
						+		" = PersonnageJouable::ramasser(ryan(GC), collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^"
						+		" collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC)) != NULL ^ personnage = ryan(GC)"
						+		"  = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Personnage::force(estFrappe(GC, ryan(GC)))), 5) si estFrappe(GC, ryan(GC)) != NULL ^ personnage = ryan(GC)"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Objet::bonusDeForce(collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))) != NULL ^ personnage = ryan(GC)"
						+       " = Personnage::geler(ryan(GC), 5) si personnage = ryan(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(ryan(GC))"
						+		" = Personnage::degeler() sinon");
			}
		}
		
		if(estFrappe(p)!= null && Toolbox.equals(p, personnage)){
			p.retirerPointsDeVie(estFrappe(p).force());
			p.geler(5);
			post = Toolbox.equals(p, ryan());
			if(!post){
				throw new PostconditionError("		ryan(gererCommande(GC, personnage,commande)) = ryan(GC) si personnage != ryan(GC) || estFrappe(GC, ryan(GC)) = NULL ^ Personnage::estGele( ryan(GC)) ^ commande = NULL "
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(max(Position::x(ryan(GC)) -1, 0)), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(min(Position::x(ryan(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele(ryan(GC)) ^ personnage = ryan(GC))"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), min(Position::y(ryan(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), max(Position::y(ryan(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Personnage::position(estPorte(GC, ryan(GC)))) si estPorte(GC, ryan(GC)) != NULL"
						+		" = PersonnageJouable::jeter(ryan(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, ryan(GC)) != NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"	 
						+		" = PersonnageJouable::ramasser(ryan(GC), collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^"
						+		" collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC)) != NULL ^ personnage = ryan(GC)"
						+		"  = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Personnage::force(estFrappe(GC, ryan(GC)))), 5) si estFrappe(GC, ryan(GC)) != NULL ^ personnage = ryan(GC)"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Objet::bonusDeForce(collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))) != NULL ^ personnage = ryan(GC)"
						+       " = Personnage::geler(ryan(GC), 5) si personnage = ryan(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(ryan(GC))"
						+		" = Personnage::degeler() sinon");
			}
		}
		
		if(Toolbox.equals(p, personnage) && collisionObjetLance(p, terrain_pre.objets()) != null){
			p.retirerPointsDeVie(collisionObjetLance(p, terrain_pre.objets()).bonusDeForce());
			p.geler(5);
			post = Toolbox.equals(p, ryan());
			if(!post){
				throw new PostconditionError("		ryan(gererCommande(GC, personnage,commande)) = ryan(GC) si personnage != ryan(GC) || estFrappe(GC, ryan(GC)) = NULL ^ Personnage::estGele( ryan(GC)) ^ commande = NULL "
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(max(Position::x(ryan(GC)) -1, 0)), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(min(Position::x(ryan(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele(ryan(GC)) ^ personnage = ryan(GC))"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), min(Position::y(ryan(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), max(Position::y(ryan(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Personnage::position(estPorte(GC, ryan(GC)))) si estPorte(GC, ryan(GC)) != NULL"
						+		" = PersonnageJouable::jeter(ryan(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, ryan(GC)) != NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"	 
						+		" = PersonnageJouable::ramasser(ryan(GC), collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^"
						+		" collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC)) != NULL ^ personnage = ryan(GC)"
						+		"  = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Personnage::force(estFrappe(GC, ryan(GC)))), 5) si estFrappe(GC, ryan(GC)) != NULL ^ personnage = ryan(GC)"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Objet::bonusDeForce(collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))) != NULL ^ personnage = ryan(GC)"
						+       " = Personnage::geler(ryan(GC), 5) si personnage = ryan(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(ryan(GC))"
						+		" = Personnage::degeler() sinon");
			}
		}
		if(Toolbox.equals(p, personnage)){
			p.degeler();
			post = Toolbox.equals(p, ryan());
			if(!post){
				throw new PostconditionError("		ryan(gererCommande(GC, personnage,commande)) = ryan(GC) si personnage != ryan(GC) || estFrappe(GC, ryan(GC)) = NULL ^ Personnage::estGele( ryan(GC)) ^ commande = NULL "
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(max(Position::x(ryan(GC)) -1, 0)), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.GAUCHE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(min(Position::x(ryan(GC))) +1, Dimensions::largeur(Terrain::dimensions(terrain(GC)))), Position::y(ryan(GC)), Position::z(ryan(GC))) si commande1 = COMMANDE.DROITE ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele(ryan(GC)) ^ personnage = ryan(GC))"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), min(Position::y(ryan(GC))+1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.HAUT ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Position::init(Position::x(ryan(GC)), max(Position::y(ryan(GC))-1, Dimensions::profondeur(Terrain::dimensions(terrain(GC)))))) si commande1 = COMMANDE.BAS ^ estFrappe(GC, ryan(GC)) = NULL  ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"
						+		" = PersonnageJouable::deplacer(ryan(GC), Personnage::position(estPorte(GC, ryan(GC)))) si estPorte(GC, ryan(GC)) != NULL"
						+		" = PersonnageJouable::jeter(ryan(GC)) si commande1 = COMMANDE.JETER ^ estFrappe(GC, ryan(GC)) != NULL ^ !Personnage::estGele( ryan(GC)) ^ personnage = ryan(GC)"	 
						+		" = PersonnageJouable::ramasser(ryan(GC), collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC))) si commande = COMMANDE.RAMASSER ^ estFrappe(GC, ryan(GC)) = NULL ^ !Personnage::estGele( ryan(GC)) ^"
						+		" collisionObjetRamasse(GC, ryan(GC), Terrain::objets(terrain(GC)) != NULL ^ personnage = ryan(GC)"
						+		"  = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Personnage::force(estFrappe(GC, ryan(GC)))), 5) si estFrappe(GC, ryan(GC)) != NULL ^ personnage = ryan(GC)"
						+		" = Personnage::geler(Personnage::retirerPointsDeVie(ryan(GC), Objet::bonusDeForce(collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))))), 5) si collisionObjetLance(GC,ryan(GC),Terrain::objets(terrain(GC))) != NULL ^ personnage = ryan(GC)"
						+       " = Personnage::geler(ryan(GC), 5) si personnage = ryan(GC) ^ commande = COMMANDE.FRAPPE ^ !Personnage::estGele(ryan(GC))"
						+		" = Personnage::degeler() sinon");
			}
		}	
	}	
}
